w:World.
FairFifo
 (e:E.
 (state_after(e;e.w-info(w;e);e.w-pred(w;e);i,x. s(i;0).x;i.1of(2of(w-machine(w;i)));e.
 (val(e))
 (=
 ((x.s(loc(e);time(e)+1).x)
 ( x:Idvartype(loc(e);x)) 

latex

Definitions	t  T, x:A. B(x), time(e), #$n, , {x:A| B(x) }, x:AB(x), n+m, a<b, Void, P  Q, False, A, AB, , Id, loc(e), s(i;t).x, x.A(x), vartype(i;x), x. t(x), 2of(t), s = t, Prop, state_after(e;info;pred?;init;Trans;val), E, FairFifo, World
Lemmas	w-when-after, world wf, fair-fifo wf, w-E wf, pi2 wf, w-vartype wf, w-s wf, w-loc wf, Id wf, nat wf, w-time wf